import ply.lex as lex

tokens = (
    'LPAREN', 'RPAREN',
    'COMMA',
    'IDENT',
    'DOT',
    'BSLASH',
    'AND',
    'OR',
    'NOT',
    )

t_DOT = r'\.'
t_BSLASH = r'\\'
t_LPAREN = r'\('
t_RPAREN = r'\)'
t_COMMA = r','

reserved = {
    'and': 'AND',
    'or': 'OR',
    'not': 'NOT',
    }    

def t_IDENT(t):
    r'[a-zA-Z_]+'
    t.type = reserved.get(t.value, 'IDENT')    
    return t

t_ignore = ' \t'

def t_newline(t):
    r'\n+'
    t.lexer.lineno += len(t.value)

def t_error(t):
    print "Illegal character '%s'" % t.value[0]
    t.lexer.skip(1)

import ply.lex as lex
lex.lex()

from cheqed.core import qterm, qtype, theory

def p_term(p):
    '''term : atom
            | combination
            | abstraction
            | operator'''
    p[0] = p[1]

precedence = (
    ('right', 'NOT'),
    ('left', 'AND'),
    ('left', 'OR'),
    )
    
def p_operator(p):
    'operator : term AND term'
    p[0] = qterm.binary_op(theory.and_, p[1], p[3])

def p_operator_or(p):
    'operator : term OR term'
    p[0] = qterm.binary_op(theory.or_, p[1], p[3])

def p_operator_not(p):
    'operator : NOT term'
    p[0] = qterm.unary_op(theory.not_, p[2])
    
def p_atom(p):
    'atom : IDENT'
    p[0] = qterm.Variable(p[1], qtype.qvar())
    
def p_abstraction(p):
    'abstraction : LPAREN BSLASH atom DOT term RPAREN'
    p[0] = qterm.Abstraction(p[3], p[5])
    
def p_arglist_empty(p):
    'arglist :'
    p[0] = []

def p_arglist_pair(p):
    'arglist : term COMMA arglist'
    p[0] = [p[1]] + p[3]

def p_arglist_term(p):
    'arglist : term'
    p[0] = [p[1]]

def p_combination(p):
    'combination : term LPAREN arglist RPAREN'
    c = p[1]
    a = p[3]
    a.reverse()
    while a:
        c = qterm.Combination(c, a.pop())
    p[0] = c

def p_error(p):
    print "Syntax error at '%s'" % p.value

import ply.yacc as yacc
yacc.yacc(start='term')
print yacc.parse(r'foo')
print yacc.parse(r'foo()')
print yacc.parse(r'foo(bar)')
print yacc.parse(r'foo(bar, baz)')
print yacc.parse(r'foo(bar, baz(bat))')
print yacc.parse(r'foo(bar)(bar, baz(bat))')
print yacc.parse(r'(\x.foo)(bar)')
print yacc.parse(r'foo and bar')
print yacc.parse(r'a and not b or c')
